1 /-
2 Copyright (c) 2018 Mario Carneiro and Kevin Buzzard. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Mario Carneiro, Kevin Buzzard
5 -/
6
7 import data.equiv.algebra
src └────────────────┘
8 import linear_algebra.finsupp
src └────────────────────┘
9 import ring_theory.ideal_operations
src └──────────────────────────┘
10 import ring_theory.subring
src └─────────────────┘
11 import linear_algebra.basis
src └──────────────────┘
12
13 open set lattice
14
15 namespace submodule
16 variables {α : Type*} {β : Type*} [ring α] [add_comm_group β] [module α β]
id └───────┘ └────┘
src └───────┘ └────┘
typ └───────┘ └────┘
doc └────┘
17
18 def fg (s : submodule α β) : Prop := ∃ t : finset β, submodule.span α ↑t = s
id └───────┘ ┴ ┴ ┴ └────┘ ┴┴ └────────────┘ ┴ ┴┴ ┴ ┴
src └───────┘ ┴ └────┘ ┴ └────────────┘ ┴ ┴
typ └───────┘ ┴ ┴ ┴ └────┘ ┴┴ └────────────┘ ┴ ┴┴ ┴ ┴
doc └───────┘ └────┘ └────────────┘
19
20 theorem fg_def {s : submodule α β} :
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
doc └───────┘
21 s.fg ↔ ∃ t : set β, finite t ∧ span α t = s :=
id ┴└─┘ ┴ ┴ └─┘ ┴┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ └─┘ ┴ └────┘ ┴ └──┘ ┴
typ ┴└─┘ ┴ ┴ └─┘ ┴┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └────┘ └──┘
22 ⟨λ ⟨t, h⟩, ⟨_, finset.finite_to_set t, h⟩, begin
id ┴┴ ┴ └──────────────────┘
src └──────────────────┘
typ ┴┴ ┴ └──────────────────┘
st └─────
23 rintro ⟨t', h, rfl⟩,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └───────────┘
st ────────────────────┘└─
24 rcases finite.exists_finset_coe h with ⟨t, rfl⟩,
id └──────────────────────┘ ┴
src └─────┘└──────────────────────┘┴ └────────────┘
typ └─────┘└──────────────────────┘┴┴└────────────┘
doc └─────┘ ┴ └────────────┘
txt └─────┘ ┴ └────────────┘
par └─────┘ ┴ └────────────┘
pid ┴ ┴ └────────────┘
st ────────────────────────────────────────────────┘└─
25 exact ⟨t, rfl⟩
id ┴ └─┘
src └────┘ └┘└─┘└┘
typ └────┘ ┴└┘└─┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴ └┘ ┴┴
st ────────────────┘
26 end⟩
st └─┘
27
28 /-- Nakayama's Lemma. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2, Stacks 00DV -/
29 theorem exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul {R : Type*} [comm_ring R]
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
30 {M : Type*} [add_comm_group M] [module R M]
id └────────────┘ ┴ └────┘ ┴ ┴
src └────────────┘ └────┘
typ └────────────┘ ┴ └────┘ ┴ ┴
doc └────┘
31 (I : ideal R) (N : submodule R M) (hn : N.fg) (hin : N ≤ I • N) :
id └───┘ ┴ └───────┘ ┴ ┴ ┴└─┘ ┴ ┴ ┴ ┴ ┴
src └───┘ └───────┘ └─┘ ┴ ┴
typ └───┘ ┴ └───────┘ ┴ ┴ ┴└─┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘
32 ∃ r : R, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = (0 : M) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
33 begin
34 rw fg_def at hn, rcases hn with ⟨s, hfs, hs⟩,
src └─┘ └────┘ └─────┘ └────────────────┘
typ └─┘ └────┘ └─────┘ └────────────────┘
doc └─┘ └────┘ └─────┘ └────────────────┘
txt └─┘ └────┘ └─────┘ └────────────────┘
par └─┘ └────┘ └─────┘ └────────────────┘
pid ┴ └────┘ ┴ └────────────────┘
35 have : ∃ r : R, r - 1 ∈ I ∧ N ≤ (I • span R s).comap (linear_map.lsmul R M r) ∧ s ⊆ N,
id ┴ └──────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └──────┘ └──────────────┘┴ ┴ ┴ └┘ ┴ ┴┴┴
typ └─────┘ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └──────┘ └──────────────┘┴┴┴┴┴ └┘ ┴┴┴┴┴┴
doc └─────┘ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └─────┘ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └─────┘ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └───┘└┘ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st └───────────────────────────────────────────┘└─
36 { refine ⟨1, _, _, _⟩,
src └─────┘ └─────────┘
typ └─────┘ └─────────┘
doc └─────┘ └─────────┘
txt └─────┘ └─────────┘
par └─────┘ └─────────┘
pid ┴ └─────────┘
st ───┘└─────────────────┘└─
37 { rw sub_self, exact I.zero_mem },
id └──────┘ └────────┘
src └─┘└──────┘ └────┘└────────┘┴
typ └─┘└──────┘ └────┘└────────┘┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st ─────┘└─────────┘└─────────────────┘└┘└
38 { rw [hs], intros n hn, rw [mem_coe, mem_comap], change (1:R) • n ∈ I • N, rw one_smul, exact hin hn },
id └┘ └─────┘ └───────┘ ┴ ┴ ┴ ┴ └──────┘ └─┘ └┘
src └──┘ ┴ └─────────┘ └──┘└─────┘└┘└───────┘┴ └─────┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └─┘└──────┘ └────┘ ┴ ┴
typ └──┘└┘┴ └─────────┘ └──┘└─────┘└┘└───────┘┴ └─────┘ └┘┴└┘ ┴┴┴ ┴┴┴ ┴┴ └─┘└──────┘ └────┘└─┘┴└┘┴
doc └──┘ ┴ └─────────┘ └──┘ └┘ ┴ └─────┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘ ┴ ┴
txt └──┘ ┴ └─────────┘ └──┘ └┘ ┴ └─────┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘ ┴ ┴
par └──┘ ┴ └─────────┘ └──┘ └┘ ┴ └─────┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘ ┴ ┴
pid └┘ ┴ └───┘ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────┘└────┘└────────────┘└───────────┘└─────────┘└─────────────────────────┘└───────────┘└─────────────┘└┘└
39 { rw [← span_le, hs], exact le_refl N } },
id └─────┘ └┘ └─────┘ ┴
src └────┘└─────┘└┘ ┴ └────┘└─────┘┴ ┴
typ └────┘└─────┘└┘└┘┴ └────┘└─────┘┴┴┴
doc └────┘ └┘ ┴ └────┘ ┴ ┴
txt └────┘ └┘ ┴ └────┘ ┴ ┴
par └────┘ └┘ ┴ └────┘ ┴ ┴
pid └──┘ └┘ ┴ ┴ ┴ ┴
st ──────────────────┘└──┘└─────────────────┘└──┘└
40 clear hin hs, revert this,
src └──────────┘ └─────────┘
typ └──────────┘ └─────────┘
doc └──────────┘ └─────────┘
txt └──────────┘ └─────────┘
par └──────────┘ └─────────┘
pid └─────┘ └───┘
st ─────────────┘└───────────┘└─
41 refine set.finite.dinduction_on hfs (λ H, _) (λ i s his hfs ih H, _),
id └──────────────────────┘ └─┘
src └─────┘└──────────────────────┘┴ ┴ └─────┘ └───────────────────┘
typ └─────┘└──────────────────────┘┴└─┘┴ └─────┘ └───────────────────┘
doc └─────┘ ┴ ┴ └─────┘ └───────────────────┘
txt └─────┘ ┴ ┴ └─────┘ └───────────────────┘
par └─────┘ ┴ ┴ └─────┘ └───────────────────┘
pid ┴ ┴ ┴ └─────┘ └───────────────────┘
st ─────────────────────────────────────────────────────────────────────┘└─
42 { rcases H with ⟨r, hr1, hrn, hs⟩, refine ⟨r, hr1, λ n hn, _⟩, specialize hrn hn,
id ┴ ┴ └─┘ └─┘ └┘
src └─────┘ └─────────────────────┘ └─────┘ └┘ └┘ └───────┘ └─────────┘ ┴
typ └─────┘┴└─────────────────────┘ └─────┘ ┴└┘└─┘└┘ └───────┘ └─────────┘└─┘┴└┘
doc └─────┘ └─────────────────────┘ └─────┘ └┘ └┘ └───────┘ └─────────┘ ┴
txt └─────┘ └─────────────────────┘ └─────┘ └┘ └┘ └───────┘ └─────────┘ ┴
par └─────┘ └─────────────────────┘ └─────┘ └┘ └┘ └───────┘ └─────────┘ ┴
pid ┴ └─────────────────────┘ ┴ └┘ └┘ └───────┘ ┴ ┴
st ───┘└─────────────────────────────┘└──────────────────────────┘└─────────────────┘└─
43 rwa [mem_coe, mem_comap, span_empty, smul_bot, mem_bot] at hrn },
id └─────┘ └───────┘ └────────┘ └──────┘ └─────┘
src └───┘└─────┘└┘└───────┘└┘└────────┘└┘└──────┘└┘└─────┘└───────┘
typ └───┘└─────┘└┘└───────┘└┘└────────┘└┘└──────┘└┘└─────┘└───────┘
doc └───┘ └┘ └┘ └┘ └┘ └───────┘
txt └───┘ └┘ └┘ └┘ └┘ └───────┘
par └───┘ └┘ └┘ └┘ └┘ └───────┘
pid └┘ └┘ └┘ └┘ └┘ ┴└─────┘┴
st ───────────────┘└─────────┘└──────────┘└────────┘└───────┘┴└──────┘└┘└
44 apply ih, rcases H with ⟨r, hr1, hrn, hs⟩,
id ┴
src └────┘ └─────┘ └─────────────────────┘
typ └────┘ └─────┘┴└─────────────────────┘
doc └────┘ └─────┘ └─────────────────────┘
txt └────┘ └─────┘ └─────────────────────┘
par └────┘ └─────┘ └─────────────────────┘
pid ┴ ┴ └─────────────────────┘
st ─────────┘└───────────────────────────────┘└─
45 rw [← set.singleton_union, span_union, smul_sup] at hrn,
id └─────────────────┘ └────────┘ └──────┘
src └────┘└─────────────────┘└┘└────────┘└┘└──────┘└──────┘
typ └────┘└─────────────────┘└┘└────────┘└┘└──────┘└──────┘
doc └────┘ └┘ └┘ └──────┘
txt └────┘ └┘ └┘ └──────┘
par └────┘ └┘ └┘ └──────┘
pid └──┘ └┘ └┘ ┴└─────┘
st ──────────────────────────┘└──────────┘└────────┘┴└─────┘└─
46 rw [set.insert_subset] at hs,
id └───────────────┘
src └──┘└───────────────┘└─────┘
typ └──┘└───────────────┘└─────┘
doc └──┘ └─────┘
txt └──┘ └─────┘
par └──┘ └─────┘
pid └┘ ┴└────┘
st ──────────────────────┘┴└────┘└─
47 have : ∃ c : R, c - 1 ∈ I ∧ c • i ∈ I • span R s,
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └─────┘┴└───┘ ┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘┴ ┴
typ └─────┘┴└───┘ ┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴┴┴ ┴└──┘┴┴┴┴
doc └─────┘ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘┴ ┴
txt └─────┘ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ └───┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────┘└─
48 { specialize hrn hs.1, rw [mem_coe, mem_comap, mem_sup] at hrn,
id └─┘ └┘ └─────┘ └───────┘ └─────┘
src └─────────┘ ┴ └┘ └──┘└─────┘└┘└───────┘└┘└─────┘└──────┘
typ └─────────┘└─┘┴└┘└┘ └──┘└─────┘└┘└───────┘└┘└─────┘└──────┘
doc └─────────┘ ┴ └┘ └──┘ └┘ └┘ └──────┘
txt └─────────┘ ┴ └┘ └──┘ └┘ └┘ └──────┘
par └─────────┘ ┴ └┘ └──┘ └┘ └┘ └──────┘
pid ┴ ┴ └┘ └┘ └┘ └┘ ┴└─────┘
st ───┘└─────────────────┘└───────────┘└─────────┘└───────┘┴└─────┘└─
49 rcases hrn with ⟨y, hy, z, hz, hyz⟩, change y + z = r • i at hyz,
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └───────────────────────┘ └─────┘ ┴┴┴ ┴┴┴ ┴ ┴ └─────┘
typ └─────┘└─┘└───────────────────────┘ └─────┘┴┴┴┴┴┴┴┴┴┴ ┴┴└─────┘
doc └─────┘ └───────────────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
txt └─────┘ └───────────────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
par └─────┘ └───────────────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
pid ┴ └───────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└────┘
st ──────────────────────────────────────┘└───────────────────────────┘└─
50 rw mem_smul_span_singleton at hy, rcases hy with ⟨c, hci, rfl⟩,
id └─────────────────────┘ └┘
src └─┘└─────────────────────┘└────┘ └─────┘ └─────────────────┘
typ └─┘└─────────────────────┘└────┘ └─────┘└┘└─────────────────┘
doc └─┘ └────┘ └─────┘ └─────────────────┘
txt └─┘ └────┘ └─────┘ └─────────────────┘
par └─┘ └────┘ └─────┘ └─────────────────┘
pid ┴ └────┘ ┴ └─────────────────┘
st ───────────────────────────────────┘└────────────────────────────┘└─
51 use r-c, split,
id ┴ ┴
src └──┘ └───┘
typ └──┘┴ ┴ └───┘
doc └──┘ └───┘
txt └──┘ └───┘
par └──┘ └───┘
pid ┴
st ──────────┘└─────┘└─
52 { rw [sub_right_comm], exact I.sub_mem hr1 hci },
id └────────────┘ └───────┘ └─┘ └─┘
src └──┘└────────────┘┴ └────┘└───────┘┴ ┴ ┴
typ └──┘└────────────┘┴ └────┘└───────┘┴└─┘┴└─┘┴
doc └──┘ ┴ └────┘ ┴ ┴ ┴
txt └──┘ ┴ └────┘ ┴ ┴ ┴
par └──┘ ┴ └────┘ ┴ ┴ ┴
pid └┘ ┴ ┴ ┴ ┴ ┴
st ─────┘└────────────────┘└─────────────────────────┘└┘└
53 { rw [sub_smul, ← hyz, add_sub_cancel'], exact hz } },
id └──────┘ └─┘ └─────────────┘ └┘
src └──┘└──────┘└──┘ └┘└─────────────┘┴ └────┘ ┴
typ └──┘└──────┘└──┘└─┘└┘└─────────────┘┴ └────┘└┘┴
doc └──┘ └──┘ └┘ ┴ └────┘ ┴
txt └──┘ └──┘ └┘ ┴ └────┘ ┴
par └──┘ └──┘ └┘ ┴ └────┘ ┴
pid └┘ └──┘ └┘ ┴ ┴ ┴
st ─────────────────┘└─────┘└───────────────┘└──────────┘└──┘└
54 rcases this with ⟨c, hc1, hci⟩, refine ⟨c * r, _, _, hs.2⟩,
id └──┘ ┴ ┴ ┴ └┘
src └─────┘ └─────────────────┘ └─────┘ ┴┴┴ └──────┘ └─┘
typ └─────┘└──┘└─────────────────┘ └─────┘ ┴┴┴┴┴└──────┘└┘└─┘
doc └─────┘ └─────────────────┘ └─────┘ ┴ ┴ └──────┘ └─┘
txt └─────┘ └─────────────────┘ └─────┘ ┴ ┴ └──────┘ └─┘
par └─────┘ └─────────────────┘ └─────┘ ┴ ┴ └──────┘ └─┘
pid ┴ └─────────────────┘ ┴ ┴ ┴ └──────┘ └─┘
st ───────────────────────────────┘└──────────────────────────┘└─
55 { rw [← ideal.quotient.eq, ideal.quotient.mk_one] at hr1 hc1 ⊢,
id └───────────────┘ └───────────────────┘
src └────┘└───────────────┘└┘└───────────────────┘└────────────┘
typ └────┘└───────────────┘└┘└───────────────────┘└────────────┘
doc └────┘ └┘ └────────────┘
txt └────┘ └┘ └────────────┘
par └────┘ └┘ └────────────┘
pid └──┘ └┘ ┴└───────────┘
st ───┘└─────────────────────┘└─────────────────────┘┴└───────────┘└─
56 rw [ideal.quotient.mk_mul, hc1, hr1, mul_one] },
id └───────────────────┘ └─┘ └─┘ └─────┘
src └──┘└───────────────────┘└┘ └┘ └┘└─────┘└┘
typ └──┘└───────────────────┘└┘└─┘└┘└─┘└┘└─────┘└┘
doc └──┘ └┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ ┴┴
st ────────────────────────────┘└───┘└───┘└───────┘┴┴└┘└
57 { intros n hn, specialize hrn hn, rw [mem_coe, mem_comap, mem_sup] at hrn,
id └─┘ └┘ └─────┘ └───────┘ └─────┘
src └─────────┘ └─────────┘ ┴ └──┘└─────┘└┘└───────┘└┘└─────┘└──────┘
typ └─────────┘ └─────────┘└─┘┴└┘ └──┘└─────┘└┘└───────┘└┘└─────┘└──────┘
doc └─────────┘ └─────────┘ ┴ └──┘ └┘ └┘ └──────┘
txt └─────────┘ └─────────┘ ┴ └──┘ └┘ └┘ └──────┘
par └─────────┘ └─────────┘ ┴ └──┘ └┘ └┘ └──────┘
pid └───┘ ┴ ┴ └┘ └┘ └┘ ┴└─────┘
st ──────────────┘└─────────────────┘└───────────┘└─────────┘└───────┘┴└─────┘└─
58 rcases hrn with ⟨y, hy, z, hz, hyz⟩, change y + z = r • n at hyz,
id └─┘ ┴ ┴ ┴ ┴
src └─────┘ └───────────────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
typ └─────┘└─┘└───────────────────────┘ └─────┘┴┴ ┴┴┴ ┴┴┴ ┴┴└─────┘
doc └─────┘ └───────────────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
txt └─────┘ └───────────────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
par └─────┘ └───────────────────────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
pid ┴ └───────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└────┘
st ──────────────────────────────────────┘└───────────────────────────┘└─
59 rw mem_smul_span_singleton at hy, rcases hy with ⟨d, hdi, rfl⟩,
id └─────────────────────┘ └┘
src └─┘└─────────────────────┘└────┘ └─────┘ └─────────────────┘
typ └─┘└─────────────────────┘└────┘ └─────┘└┘└─────────────────┘
doc └─┘ └────┘ └─────┘ └─────────────────┘
txt └─┘ └────┘ └─────┘ └─────────────────┘
par └─┘ └────┘ └─────┘ └─────────────────┘
pid ┴ └────┘ ┴ └─────────────────┘
st ───────────────────────────────────┘└────────────────────────────┘└─
60 change _ • _ ∈ I • span R s,
id ┴ └──┘ ┴ ┴
src └───────┘ └─┘ ┴ ┴ ┴└──┘┴ ┴
typ └───────┘ └─┘ ┴┴┴ ┴└──┘┴┴┴┴
doc └───────┘ └─┘ ┴ ┴ ┴└──┘┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴ ┴ ┴
pid └─┘ └─┘ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────┘└─
61 rw [mul_smul, ← hyz, smul_add, smul_smul, mul_comm, mul_smul],
id └──────┘ └─┘ └──────┘ └───────┘ └──────┘ └──────┘
src └──┘└──────┘└──┘ └┘└──────┘└┘└───────┘└┘└──────┘└┘└──────┘┴
typ └──┘└──────┘└──┘└─┘└┘└──────┘└┘└───────┘└┘└──────┘└┘└──────┘┴
doc └──┘ └──┘ └┘ └┘ └┘ └┘ ┴
txt └──┘ └──┘ └┘ └┘ └┘ └┘ ┴
par └──┘ └──┘ └┘ └┘ └┘ └┘ ┴
pid └┘ └──┘ └┘ └┘ └┘ └┘ ┴
st ───────────────┘└─────┘└────────┘└─────────┘└────────┘└────────┘└──
62 exact add_mem _ (smul_mem _ _ hci) (smul_mem _ _ hz) }
id └─────┘ └─┘ └──────┘ └┘
src └────┘└─────┘└─┘ └───┘ └┘ └──────┘└───┘ └┘
typ └────┘└─────┘└─┘ └───┘└─┘└┘ └──────┘└───┘└┘└┘
doc └────┘ └─┘ └───┘ └┘ └───┘ └┘
txt └────┘ └─┘ └───┘ └┘ └───┘ └┘
par └────┘ └─┘ └───┘ └┘ └───┘ └┘
pid ┴ └─┘ └───┘ └┘ └───┘ ┴┴
st ────────────────────────────────────────────────────────┘└─
63 end
st ──┘
64
65 theorem fg_bot : (⊥ : submodule α β).fg :=
id ┴ └───────┘ ┴ ┴ └┘
src ┴ └───────┘ └┘
typ ┴ └───────┘ ┴ ┴ └┘
doc └───────┘
66 ⟨∅, by rw [finset.coe_empty, span_empty]⟩
id ┴ └──────────────┘ └────────┘
src ┴ └──┘└──────────────┘└┘└────────┘┴
typ ┴ └──┘└──────────────┘└┘└────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └───────────────────┘└──────────┘┴
67
68 theorem fg_sup {s₁ s₂ : submodule α β}
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
doc └───────┘
69 (hs₁ : s₁.fg) (hs₂ : s₂.fg) : (s₁ ⊔ s₂).fg :=
id └┘└─┘ └┘└─┘ └┘ ┴ └┘ └┘
src └─┘ └─┘ ┴ └┘
typ └┘└─┘ └┘└─┘ └┘ ┴ └┘ └┘
70 let ⟨t₁, ht₁⟩ := fg_def.1 hs₁, ⟨t₂, ht₂⟩ := fg_def.1 hs₂ in
id └─┘ └┘ └─┘ └────┘┴ └─┘ └┘ └─┘ └────┘┴ └─┘
src └────┘┴ └────┘┴
typ └─┘ └┘ └─┘ └────┘┴ └─┘ └┘ └─┘ └────┘┴ └─┘
71 fg_def.2 ⟨t₁ ∪ t₂, finite_union ht₁.1 ht₂.1, by rw [span_union, ht₁.2, ht₂.2]⟩
id └────┘┴ ┴ └──────────┘ ┴ ┴ └────────┘ └─┘ └─┘
src └────┘┴ ┴ └──────────┘ ┴ ┴ └──┘└────────┘└┘ └──┘ └─┘
typ └────┘┴ ┴ └──────────┘ ┴ ┴ └──┘└────────┘└┘└─┘└──┘└─┘└─┘
doc └──┘ └┘ └──┘ └─┘
txt └──┘ └┘ └──┘ └─┘
par └──┘ └┘ └──┘ └─┘
pid └┘ └┘ └──┘ └─┘
st └─────────────┘└───┘└─────┘└─┘
72
73 variables {γ : Type*} [add_comm_group γ] [module α γ]
id └────────────┘ └────┘
src └────────────┘ └────┘
typ └────────────┘ └────┘
doc └────┘
74 variables {f : β →ₗ[α] γ}
id └─┘ ┴
src └─┘ ┴
typ └─┘ ┴
75
76 theorem fg_map {s : submodule α β} (hs : s.fg) : (s.map f).fg :=
id └───────┘ ┴ ┴ ┴└─┘ ┴└──┘ ┴ └┘
src └───────┘ └─┘ └──┘ └┘
typ └───────┘ ┴ ┴ ┴└─┘ ┴└──┘ ┴ └┘
doc └───────┘ └──┘
77 let ⟨t, ht⟩ := fg_def.1 hs in fg_def.2 ⟨f '' t, finite_image _ ht.1, by rw [span_image, ht.2]⟩
id └─┘ ┴ └┘ └────┘┴ └┘ └────┘┴ ┴ └┘ └──────────┘ ┴ └────────┘ └┘
src └────┘┴ └────┘┴ └┘ └──────────┘ ┴ └──┘└────────┘└┘ └─┘
typ └─┘ ┴ └┘ └────┘┴ └┘ └────┘┴ ┴ └┘ └──────────┘ ┴ └──┘└────────┘└┘└┘└─┘
doc └──┘ └┘ └─┘
txt └──┘ └┘ └─┘
par └──┘ └┘ └─┘
pid └┘ └┘ └─┘
st └─────────────┘└──┘└─┘
78
79 theorem fg_prod {sb : submodule α β} {sc : submodule α γ}
id └───────┘ ┴ ┴ └───────┘ ┴ ┴
src └───────┘ └───────┘
typ └───────┘ ┴ ┴ └───────┘ ┴ ┴
doc └───────┘ └───────┘
80 (hsb : sb.fg) (hsc : sc.fg) : (sb.prod sc).fg :=
id └┘└─┘ └┘└─┘ └┘└───┘ └┘ └┘
src └─┘ └─┘ └───┘ └┘
typ └┘└─┘ └┘└─┘ └┘└───┘ └┘ └┘
doc └───┘
81 let ⟨tb, htb⟩ := fg_def.1 hsb, ⟨tc, htc⟩ := fg_def.1 hsc in
id └─┘ └┘ └─┘ └────┘┴ └─┘ └┘ └─┘ └────┘┴ └─┘
src └────┘┴ └┘ └────┘┴
typ └─┘ └┘ └─┘ └────┘┴ └─┘ └┘ └─┘ └────┘┴ └─┘
82 fg_def.2 ⟨prod.inl '' tb ∪ prod.inr '' tc,
id └────┘┴ └──────┘ └┘ ┴ └──────┘ └┘
src └────┘┴ └──────┘ └┘ ┴ └──────┘ └┘
typ └────┘┴ └──────┘ └┘ ┴ └──────┘ └┘
doc └──────┘ └──────┘
83 finite_union (finite_image _ htb.1) (finite_image _ htc.1),
id └──────────┘ └──────────┘ ┴ └──────────┘ ┴
src └──────────┘ └──────────┘ ┴ └──────────┘ ┴
typ └──────────┘ └──────────┘ ┴ └──────────┘ ┴
84 by rw [linear_map.span_inl_union_inr, htb.2, htc.2]⟩
id └───────────────────────────┘ └─┘ └─┘
src └──┘└───────────────────────────┘└┘ └──┘ └─┘
typ └──┘└───────────────────────────┘└┘└─┘└──┘└─┘└─┘
doc └──┘ └┘ └──┘ └─┘
txt └──┘ └┘ └──┘ └─┘
par └──┘ └┘ └──┘ └─┘
pid └┘ └┘ └──┘ └─┘
st └────────────────────────────────┘└───┘└─────┘└─┘
85
86 variable (f)
87 /-- If 0 → M' → M → M'' → 0 is exact and M' and M'' are
88 finitely generated then so is M. -/
89 theorem fg_of_fg_map_of_fg_inf_ker {s : submodule α β}
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
doc └───────┘
90 (hs1 : (s.map f).fg) (hs2 : (s ⊓ f.ker).fg) : s.fg :=
id ┴└──┘ ┴ └┘ ┴ ┴ ┴└──┘ └┘ ┴└─┘
src └──┘ └┘ ┴ └──┘ └┘ └─┘
typ ┴└──┘ ┴ └┘ ┴ ┴ ┴└──┘ └┘ ┴└─┘
doc └──┘ └──┘
91 begin
st └─────
92 haveI := classical.dec_eq α, haveI := classical.dec_eq β, haveI := classical.dec_eq γ,
id └──────────────┘ ┴ └──────────────┘ ┴ └──────────────┘ ┴
src └───────┘└──────────────┘┴ └───────┘└──────────────┘┴ └───────┘└──────────────┘┴
typ └───────┘└──────────────┘┴┴ └───────┘└──────────────┘┴┴ └───────┘└──────────────┘┴┴
doc └───────┘ ┴ └───────┘ ┴ └───────┘ ┴
txt └───────┘ ┴ └───────┘ ┴ └───────┘ ┴
par └───────┘ ┴ └───────┘ ┴ └───────┘ ┴
pid ┴└─┘ ┴ ┴└─┘ ┴ ┴└─┘ ┴
st ────────────────────────────┘└───────────────────────────┘└───────────────────────────┘└─
93 cases hs1 with t1 ht1, cases hs2 with t2 ht2,
id └─┘ └─┘
src └────┘ └──────────┘ └────┘ └──────────┘
typ └────┘└─┘└──────────┘ └────┘└─┘└──────────┘
doc └────┘ └──────────┘ └────┘ └──────────┘
txt └────┘ └──────────┘ └────┘ └──────────┘
par └────┘ └──────────┘ └────┘ └──────────┘
pid ┴ └──────────┘ ┴ └──────────┘
st ──────────────────────┘└─────────────────────┘└─
94 have : ∀ y ∈ t1, ∃ x ∈ s, f x = y,
id └┘ ┴ ┴┴ ┴ ┴
src └─────┘ └───┘ ┴┴└───┘ ┴┴ ┴ ┴┴┴
typ └─────┘ └───┘└┘ ┴┴└───┘┴┴┴┴┴ ┴┴┴
doc └─────┘ └───┘ ┴ └───┘ ┴ ┴ ┴ ┴
txt └─────┘ └───┘ ┴ └───┘ ┴ ┴ ┴ ┴
par └─────┘ └───┘ ┴ └───┘ ┴ ┴ ┴ ┴
pid └───┘└┘ └───┘ ┴ └───┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
95 { intros y hy,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ───┘└─────────┘└─
96 have : y ∈ map f s, { rw ← ht1, exact subset_span hy },
id ┴ └─┘ ┴ ┴ └─┘ └─────────┘ └┘
src └─────┘ ┴ ┴└─┘┴ ┴ └───┘ └────┘└─────────┘┴ ┴
typ └─────┘┴┴ ┴└─┘┴┴┴┴ └───┘└─┘ └────┘└─────────┘┴└┘┴
doc └─────┘ ┴ ┴└─┘┴ ┴ └───┘ └────┘ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └───┘ └────┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ └───┘ └────┘ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
st ─────────────────────┘└──┘└──────┘└─────────────────────┘└┘└
97 rcases mem_map.1 this with ⟨x, hx1, hx2⟩,
id └─────┘ └──┘
src └─────┘└─────┘└─┘ └─────────────────┘
typ └─────┘└─────┘└─┘└──┘└─────────────────┘
doc └─────┘ └─┘ └─────────────────┘
txt └─────┘ └─┘ └─────────────────┘
par └─────┘ └─┘ └─────────────────┘
pid ┴ └─┘ └─────────────────┘
st ───────────────────────────────────────────┘└─
98 exact ⟨x, hx1, hx2⟩ },
id ┴ └─┘ └─┘
src └────┘ └┘ └┘ └┘
typ └────┘ ┴└┘└─┘└┘└─┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴ └┘ └┘ ┴┴
st ───────────────────────┘└┘└
99 have : ∃ g : γ → β, ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y,
id ┴ ┴ ┴ ┴┴ └┘ ┴ ┴
src └─────┘┴└───┘ ┴ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
typ └─────┘┴└───┘┴┴┴┴┴┴┴ └───┘└┘ ┴ ┴ ┴ ┴┴┴ ┴┴┴ ┴ └┘ ┴
doc └─────┘ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
txt └─────┘ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
par └─────┘ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
pid └───┘└┘ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────────┘└─
100 { choose g hg1 hg2,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └┘└──────┘
st ───┘└──────────────┘└─
101 existsi λ y, if H : y ∈ t1 then g y H else 0,
id └┘ └┘ ┴
src └──────┘ └──┘└┘└───┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
typ └──────┘ └──┘└┘└───┘ ┴ ┴└┘└────┘┴┴ ┴ └─────┘
doc └──────┘ └──┘ └───┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
txt └──────┘ └──┘ └───┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
par └──────┘ └──┘ └───┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
pid ┴ └──┘ └───┘ ┴ ┴ └────┘ ┴ ┴ └────┘┴
st ───────────────────────────────────────────────┘└─
102 intros y H, split,
src └────────┘ └───┘
typ └────────┘ └───┘
doc └────────┘ └───┘
txt └────────┘ └───┘
par └────────┘ └───┘
pid └──┘
st ─────────────┘└─────┘└─
103 { simp only [dif_pos H], apply hg1 },
id └─────┘ ┴
src └─────────┘└─────┘┴ ┴ └────┘ ┴
typ └─────────┘└─────┘┴┴┴ └────┘ ┴
doc └─────────┘ ┴ ┴ └────┘ ┴
txt └─────────┘ ┴ ┴ └────┘ ┴
par └─────────┘ ┴ ┴ └────┘ ┴
pid ┴└──┘└┘ ┴ ┴ ┴ ┴
st ─────┘└───────────────────┘└──────────┘└┘└
104 { simp only [dif_pos H], apply hg2 } },
id └─────┘ ┴
src └─────────┘└─────┘┴ ┴ └────┘ ┴
typ └─────────┘└─────┘┴┴┴ └────┘ ┴
doc └─────────┘ ┴ ┴ └────┘ ┴
txt └─────────┘ ┴ ┴ └────┘ ┴
par └─────────┘ ┴ ┴ └────┘ ┴
pid ┴└──┘└┘ ┴ ┴ ┴ ┴
st ──────────────────────────┘└──────────┘└──┘└
105 cases this with g hg, clear this,
id └──┘
src └────┘ └────────┘ └────────┘
typ └────┘└──┘└────────┘ └────────┘
doc └────┘ └────────┘ └────────┘
txt └────┘ └────────┘ └────────┘
par └────┘ └────────┘ └────────┘
pid ┴ └────────┘ └───┘
st ─────────────────────┘└──────────┘└─
106 existsi t1.image g ∪ t2,
id └──────┘ ┴ ┴ └┘
src └──────┘└──────┘┴ ┴┴┴
typ └──────┘└──────┘┴┴┴┴┴└┘
doc └──────┘└──────┘┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────┘└─
107 rw [finset.coe_union, span_union, finset.coe_image],
id └──────────────┘ └────────┘ └──────────────┘
src └──┘└──────────────┘└┘└────────┘└┘└──────────────┘┴
typ └──┘└──────────────┘└┘└────────┘└┘└──────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ─────────────────────┘└──────────┘└────────────────┘└──
108 apply le_antisymm,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────┘└─
109 { refine sup_le (span_le.2 $ image_subset_iff.2 _) (span_le.2 _),
id └────┘ └──────────────┘ └─────┘
src └─────┘└────┘┴ └─┘ ┴└──────────────┘└────┘ └─────┘└───┘
typ └─────┘└────┘┴ └─┘ ┴└──────────────┘└────┘ └─────┘└───┘
doc └─────┘ ┴ └─┘ ┴└──────────────┘└────┘ └───┘
txt └─────┘ ┴ └─┘ ┴ └────┘ └───┘
par └─────┘ ┴ └─┘ ┴ └────┘ └───┘
pid ┴ ┴ └─┘ ┴ └────┘ └───┘
st ───┘└────────────────────────────────────────────────────────────┘└─
110 { intros y hy, exact (hg y hy).1 },
id └┘ ┴ └┘
src └─────────┘ └────┘ ┴ ┴ └──┘
typ └─────────┘ └────┘ └┘┴┴┴└┘└──┘
doc └─────────┘ └────┘ ┴ ┴ └──┘
txt └─────────┘ └────┘ ┴ ┴ └──┘
par └─────────┘ └────┘ ┴ ┴ └──┘
pid └───┘ ┴ ┴ ┴ ┴└─┘
st ─────┘└─────────┘└──────────────────┘└┘└
111 { intros x hx, have := subset_span hx,
id └─────────┘ └┘
src └─────────┘ └──────┘└─────────┘┴
typ └─────────┘ └──────┘└─────────┘┴└┘
doc └─────────┘ └──────┘ ┴
txt └─────────┘ └──────┘ ┴
par └─────────┘ └──────┘ ┴
pid └───┘ └───┘└─┘ ┴
st ────────────────┘└──────────────────────┘└─
112 rw ht2 at this,
id └─┘
src └─┘ └──────┘
typ └─┘└─┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ───────────────────┘└─
113 exact this.1 } },
id └──┘
src └────┘ └─┘
typ └────┘└──┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ──────────────────┘└──┘└
114 intros x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
115 have : f x ∈ map f s, { rw mem_map, exact ⟨x, hx, rfl⟩ },
id ┴ └─┘ ┴ ┴ └─────┘ ┴ └┘ └─┘
src └─────┘ ┴ ┴ ┴└─┘┴ ┴ └─┘└─────┘ └────┘ └┘ └┘└─┘└┘
typ └─────┘ ┴┴┴ ┴└─┘┴┴┴┴ └─┘└─────┘ └────┘ ┴└┘└┘└┘└─┘└┘
doc └─────┘ ┴ ┴ ┴└─┘┴ ┴ └─┘ └────┘ └┘ └┘ └┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘ └┘ └┘ └┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘ └┘ └┘ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴┴
st ─────────────────────┘└──┘└────────┘└───────────────────┘└┘└
116 rw [← ht1,← set.image_id ↑t1, finsupp.mem_span_iff_total] at this,
id └─┘ └──────────┘ ┴└┘ └────────────────────────┘
src └────┘ └─┘└──────────┘┴┴ └┘└────────────────────────┘└───────┘
typ └────┘└─┘└─┘└──────────┘┴┴└┘└┘└────────────────────────┘└───────┘
doc └────┘ └─┘ ┴ └┘ └───────┘
txt └────┘ └─┘ ┴ └┘ └───────┘
par └────┘ └─┘ ┴ └┘ └───────┘
pid └──┘ └─┘ ┴ └┘ ┴└──────┘
st ──────────┘└─────────────────┘└──────────────────────────┘┴└──────┘└─
117 rcases this with ⟨l, hl1, hl2⟩,
id └──┘
src └─────┘ └─────────────────┘
typ └─────┘└──┘└─────────────────┘
doc └─────┘ └─────────────────┘
txt └─────┘ └─────────────────┘
par └─────┘ └─────────────────┘
pid ┴ └─────────────────┘
st ───────────────────────────────┘└─
118 refine mem_sup.2 ⟨(finsupp.total β β α id).to_fun ((finsupp.lmap_domain α α g : (γ →₀ α) → β →₀ α) l), _,
id └─────┘ └┘
src └─────┘└─────┘└─┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴└┘┴ └┘ ┴ ┴ ┴ └┘ └─────
typ └─────┘└─────┘└─┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴└┘┴ └┘ ┴ ┴ ┴ └┘ └─────
doc └─────┘ └─┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴└┘┴ └┘ ┴ ┴ ┴ └┘ └─────
txt └─────┘ └─┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └─────
par └─────┘ └─┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └─────
pid ┴ └─┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └─────
st ────────────────────────────────────────────────────────────────────────────────────────────────────────────
119 x - finsupp.total β β α id ((finsupp.lmap_domain α α g : (γ →₀ α) → β →₀ α) l), _, add_sub_cancel'_right _ _⟩,
id ┴ ┴ └───────────┘ └┘ └─────────────────┘ ┴ ┴ ┴ ┴ ┴ └───────────────────┘
src ───┘ ┴┴┴└───────────┘┴ ┴ ┴ ┴└┘┴ └─────────────────┘┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └────┘└───────────────────┘└───┘
typ ───┘┴┴┴┴└───────────┘┴ ┴ ┴ ┴└┘┴ └─────────────────┘┴ ┴┴┴┴└─┘ ┴┴ ┴ └┘ ┴┴┴ ┴ └┘┴└────┘└───────────────────┘└───┘
doc ───┘ ┴ ┴└───────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └────┘ └───┘
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └────┘ └───┘
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └────┘ └───┘
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └────┘ └───┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
120 { rw [← set.image_id (g '' ↑t1), finsupp.mem_span_iff_total], refine ⟨_, _, rfl⟩,
id └──────────┘ ┴ └┘ └┘ └────────────────────────┘ └─┘
src └────┘└──────────┘┴ ┴└┘┴ └─┘└────────────────────────┘┴ └─────┘ └────┘└─┘┴
typ └────┘└──────────┘┴ ┴┴└┘┴ └┘└─┘└────────────────────────┘┴ └─────┘ └────┘└─┘┴
doc └────┘ ┴ ┴ ┴ └─┘ ┴ └─────┘ └────┘ ┴
txt └────┘ ┴ ┴ ┴ └─┘ ┴ └─────┘ └────┘ ┴
par └────┘ ┴ ┴ ┴ └─┘ ┴ └─────┘ └────┘ ┴
pid └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ └────┘ ┴
st ───┘└───────────────────────────┘└──────────────────────────┘└───────────────────┘└─
121 haveI : inhabited γ := ⟨0⟩,
id └───────┘ ┴
src └──────┘└───────┘┴ └──┘ └┘
typ └──────┘└───────┘┴┴└──┘ └┘
doc └──────┘ ┴ └──┘ └┘
txt └──────┘ ┴ └──┘ └┘
par └──────┘ ┴ └──┘ └┘
pid ┴└┘ ┴ └──┘ └┘
st ─────────────────────────────┘└─
122 rw [← finsupp.lmap_domain_supported _ _ g, mem_map],
id └───────────────────────────┘ ┴ └─────┘
src └────┘└───────────────────────────┘└───┘ └┘└─────┘┴
typ └────┘└───────────────────────────┘└───┘┴└┘└─────┘┴
doc └────┘ └───┘ └┘ ┴
txt └────┘ └───┘ └┘ ┴
par └────┘ └───┘ └┘ ┴
pid └──┘ └───┘ └┘ ┴
st ────────────────────────────────────────────┘└───────┘└──
123 refine ⟨l, hl1, _⟩,
id ┴ └─┘
src └─────┘ └┘ └──┘
typ └─────┘ ┴└┘└─┘└──┘
doc └─────┘ └┘ └──┘
txt └─────┘ └┘ └──┘
par └─────┘ └┘ └──┘
pid ┴ └┘ └──┘
st ─────────────────────┘└─
124 refl, },
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└──┘└
125 rw [ht2, mem_inf], split,
id └─┘ └─────┘
src └──┘ └┘└─────┘┴ └───┘
typ └──┘└─┘└┘└─────┘┴ └───┘
doc └──┘ └┘ ┴ └───┘
txt └──┘ └┘ ┴ └───┘
par └──┘ └┘ ┴ └───┘
pid └┘ └┘ ┴
st ────────┘└───────┘└──────┘└─
126 { apply s.sub_mem hx,
id └───────┘ └┘
src └────┘└───────┘┴
typ └────┘└───────┘┴└┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└────────────────┘└─
127 rw [finsupp.total_apply, finsupp.lmap_domain_apply, finsupp.sum_map_domain_index],
id └─────────────────┘ └───────────────────────┘ └──────────────────────────┘
src └──┘└─────────────────┘└┘└───────────────────────┘└┘└──────────────────────────┘┴
typ └──┘└─────────────────┘└┘└───────────────────────┘└┘└──────────────────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ──────────────────────────┘└─────────────────────────┘└────────────────────────────┘└──
128 refine s.sum_mem _,
id └───────┘
src └─────┘└───────┘└┘
typ └─────┘└───────┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴ └┘
st ─────────────────────┘└─
129 { intros y hy, exact s.smul_mem _ (hg y (hl1 hy)).1 },
id └────────┘ └┘ ┴ └─┘ └┘
src └─────────┘ └────┘└────────┘└─┘ ┴ ┴ ┴ └───┘
typ └─────────┘ └────┘└────────┘└─┘ └┘┴┴┴ └─┘┴└┘└───┘
doc └─────────┘ └────┘ └─┘ ┴ ┴ ┴ └───┘
txt └─────────┘ └────┘ └─┘ ┴ ┴ ┴ └───┘
par └─────────┘ └────┘ └─┘ ┴ ┴ ┴ └───┘
pid └───┘ ┴ └─┘ ┴ ┴ ┴ └┘└─┘
st ─────┘└─────────┘└─────────────────────────────────────┘└┘└
130 { exact zero_smul _ }, { exact λ _ _ _, add_smul _ _ _ } },
id └───────┘ └──────┘
src └────┘└───────┘└─┘ └────┘ └──────┘└──────┘└─────┘
typ └────┘└───────┘└─┘ └────┘ └──────┘└──────┘└─────┘
doc └────┘ └─┘ └────┘ └──────┘ └─────┘
txt └────┘ └─┘ └────┘ └──────┘ └─────┘
par └────┘ └─┘ └────┘ └──────┘ └─────┘
pid ┴ └┘┴ ┴ └──────┘ └────┘┴
st ─────┘└────────────────┘└┘└───────────────────────────────┘└──┘└
131 { rw [linear_map.mem_ker, f.map_sub, ← hl2],
id └────────────────┘ └─┘
src └──┘└────────────────┘└┘ └──┘ ┴
typ └──┘└────────────────┘└┘└───────┘└──┘└─┘┴
doc └──┘ └┘ └──┘ ┴
txt └──┘ └┘ └──┘ ┴
par └──┘ └┘ └──┘ ┴
pid └┘ └┘ └──┘ ┴
st ─────────────────────────┘└─────────┘└─────┘└──
132 rw [finsupp.total_apply, finsupp.total_apply, finsupp.lmap_domain_apply],
id └─────────────────┘ └─────────────────┘ └───────────────────────┘
src └──┘└─────────────────┘└┘└─────────────────┘└┘└───────────────────────┘┴
typ └──┘└─────────────────┘└┘└─────────────────┘└┘└───────────────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ──────────────────────────┘└───────────────────┘└─────────────────────────┘└──
133 rw [finsupp.sum_map_domain_index, finsupp.sum, finsupp.sum, f.map_sum],
id └──────────────────────────┘ └─────────┘ └─────────┘
src └──┘└──────────────────────────┘└┘└─────────┘└┘└─────────┘└┘ ┴
typ └──┘└──────────────────────────┘└┘└─────────┘└┘└─────────┘└┘└───────┘┴
doc └──┘ └┘└─────────┘└┘└─────────┘└┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st ───────────────────────────────────┘└───────────┘└───────────┘└─────────┘└──
134 rw sub_eq_zero,
id └─────────┘
src └─┘└─────────┘
typ └─┘└─────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────┘└─
135 refine finset.sum_congr rfl (λ y hy, _),
id └──────────────┘ └─┘
src └─────┘└──────────────┘┴└─┘┴ └───────┘
typ └─────┘└──────────────┘┴└─┘┴ └───────┘
doc └─────┘ ┴ ┴ └───────┘
txt └─────┘ ┴ ┴ └───────┘
par └─────┘ ┴ ┴ └───────┘
pid ┴ ┴ ┴ └───────┘
st ──────────────────────────────────────────┘└─
136 unfold id,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid └─┘
st ────────────┘└─
137 rw [f.map_smul, (hg y (hl1 hy)).2],
id └┘ ┴ └─┘ └┘
src └──┘ └┘ ┴ ┴ ┴ └───┘
typ └──┘└────────┘└┘ └┘┴┴┴ └─┘┴└┘└───┘
doc └──┘ └┘ ┴ ┴ ┴ └───┘
txt └──┘ └┘ ┴ ┴ ┴ └───┘
par └──┘ └┘ ┴ ┴ ┴ └───┘
pid └┘ └┘ ┴ ┴ ┴ └───┘
st ─────────────────┘└───────────────┘└────
138 { exact zero_smul _ }, { exact λ _ _ _, add_smul _ _ _ } }
id └───────┘ └──────┘
src └────┘└───────┘└─┘ └────┘ └──────┘└──────┘└─────┘
typ └────┘└───────┘└─┘ └────┘ └──────┘└──────┘└─────┘
doc └────┘ └─┘ └────┘ └──────┘ └─────┘
txt └────┘ └─┘ └────┘ └──────┘ └─────┘
par └────┘ └─┘ └────┘ └──────┘ └─────┘
pid ┴ └┘┴ ┴ └──────┘ └────┘┴
st ─────┘└────────────────┘└┘└───────────────────────────────┘└───
139 end
st ──┘
140
141 end submodule
142
143 class is_noetherian (α β) [ring α] [add_comm_group β] [module α β] : Prop :=
id ┴ ┴ └──┘ ┴ └────────────┘ ┴ └────┘ ┴ ┴
src └──┘ └────────────┘ └────┘
typ ┴ ┴ └──┘ ┴ └────────────┘ ┴ └────┘ ┴ ┴
doc └────┘
144 (noetherian : ∀ (s : submodule α β), s.fg)
id ┴ └───────┘ ┴ ┴ ┴└─┘
src └───────┘ └─┘
typ ┴ └───────┘ ┴ ┴ ┴└─┘
doc └───────┘
145
146 section
147 variables {α : Type*} {β : Type*} {γ : Type*}
id ┴
typ ┴
148 variables [ring α] [add_comm_group β] [add_comm_group γ]
id └──┘ ┴└────────────┘ └────────────┘
src └──┘ └────────────┘ └────────────┘
typ └──┘ ┴└────────────┘ └────────────┘
149 variables [module α β] [module α γ]
id └────┘ └────┘
src └────┘ └────┘
typ └────┘ └────┘
doc └────┘ └────┘
150 open is_noetherian
151 include α
152
153 theorem is_noetherian_submodule {N : submodule α β} :
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
doc └───────┘
154 is_noetherian α N ↔ ∀ s : submodule α β, s ≤ N → s.fg :=
id └───────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴└─┘
src └───────────┘ ┴ └───────┘ ┴ └─┘
typ └───────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴└─┘
doc └───────┘
155 ⟨λ ⟨hn⟩, λ s hs, have s ≤ N.subtype.range, from (N.range_subtype).symm ▸ hs,
id ┴└┘ ┴ └┘ ┴ ┴ ┴└──────┘└────┘ ┴└────────────┘ └──┘ ┴ └┘
src ┴ └──────┘└────┘ └────────────┘ └──┘ ┴
typ ┴└┘ ┴ └┘ ┴ ┴ ┴└──────┘└────┘ ┴└────────────┘ └──┘ ┴ └┘
doc └────┘
156 linear_map.map_comap_eq_self this ▸ submodule.fg_map (hn _),
id └──────────────────────────┘ └──┘ ┴ └──────────────┘
src └──────────────────────────┘ ┴ └──────────────┘
typ └──────────────────────────┘ └──┘ ┴ └──────────────┘
157 λ h, ⟨λ s, submodule.fg_of_fg_map_of_fg_inf_ker N.subtype (h _ $ submodule.map_subtype_le _ _) $
id ┴ ┴ └──────────────────────────────────┘ ┴└──────┘ ┴ └──────────────────────┘
src └──────────────────────────────────┘ └──────┘ └──────────────────────┘
typ ┴ ┴ └──────────────────────────────────┘ ┴└──────┘ ┴ └──────────────────────┘
doc └──────────────────────────────────┘
158 by rw [submodule.ker_subtype, inf_bot_eq]; exact submodule.fg_bot⟩⟩
id └───────────────────┘ └────────┘ └──────────────┘
src └──┘└───────────────────┘└┘└────────┘┴ └────┘└──────────────┘
typ └──┘└───────────────────┘└┘└────────┘┴ └────┘└──────────────┘
doc └──┘ └┘ ┴ └────┘
txt └──┘ └┘ ┴ └────┘
par └──┘ └┘ ┴ └────┘
pid └┘ └┘ ┴ ┴
st └────────────────────────┘└──────────┘┴└──────────────────────┘
159
160 theorem is_noetherian_submodule_left {N : submodule α β} :
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
doc └───────┘
161 is_noetherian α N ↔ ∀ s : submodule α β, (N ⊓ s).fg :=
id └───────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └┘
src └───────────┘ ┴ └───────┘ ┴ └┘
typ └───────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └┘
doc └───────┘
162 is_noetherian_submodule.trans
id └─────────────────────┘└────┘
src └─────────────────────┘└────┘
typ └─────────────────────┘└────┘
163 ⟨λ H s, H _ inf_le_left, λ H s hs, (inf_of_le_right hs) ▸ H _⟩
id ┴ ┴ ┴ └─────────┘ ┴ ┴ └┘ └─────────────┘ └┘ ┴ ┴
src └─────────┘ └─────────────┘ ┴
typ ┴ ┴ ┴ └─────────┘ ┴ ┴ └┘ └─────────────┘ └┘ ┴ ┴
164
165 theorem is_noetherian_submodule_right {N : submodule α β} :
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
doc └───────┘
166 is_noetherian α N ↔ ∀ s : submodule α β, (s ⊓ N).fg :=
id └───────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └┘
src └───────────┘ ┴ └───────┘ ┴ └┘
typ └───────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └┘
doc └───────┘
167 is_noetherian_submodule.trans
id └─────────────────────┘└────┘
src └─────────────────────┘└────┘
typ └─────────────────────┘└────┘
168 ⟨λ H s, H _ inf_le_right, λ H s hs, (inf_of_le_left hs) ▸ H _⟩
id ┴ ┴ ┴ └──────────┘ ┴ ┴ └┘ └────────────┘ └┘ ┴ ┴
src └──────────┘ └────────────┘ ┴
typ ┴ ┴ ┴ └──────────┘ ┴ ┴ └┘ └────────────┘ └┘ ┴ ┴
169
170 variable (β)
171 theorem is_noetherian_of_surjective (f : β →ₗ[α] γ) (hf : f.range = ⊤)
id ┴ └─┘┴┴ ┴ ┴└────┘ ┴ ┴
src └─┘ ┴ └────┘ ┴ ┴
typ ┴ └─┘┴┴ ┴ ┴└────┘ ┴ ┴
doc └────┘
172 [is_noetherian α β] : is_noetherian α γ :=
id └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
src └───────────┘ └───────────┘
typ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
173 ⟨λ s, have (s.comap f).map f = s, from linear_map.map_comap_eq_self $ hf.symm ▸ le_top,
id ┴ ┴└────┘ ┴ └─┘ ┴ ┴ ┴ └──────────────────────────┘ └┘└───┘ ┴ └────┘
src └────┘ └─┘ ┴ └──────────────────────────┘ └───┘ ┴ └────┘
typ ┴ ┴└────┘ ┴ └─┘ ┴ ┴ ┴ └──────────────────────────┘ └┘└───┘ ┴ └────┘
doc └────┘ └─┘
174 this ▸ submodule.fg_map $ noetherian _⟩
id └──┘ ┴ └──────────────┘ └────────┘
src ┴ └──────────────┘ └────────┘
typ └──┘ ┴ └──────────────┘ └────────┘
175 variable {β}
176
177 theorem is_noetherian_of_linear_equiv (f : β ≃ₗ[α] γ)
id ┴ └─┘┴┴ ┴
src └─┘ ┴
typ ┴ └─┘┴┴ ┴
doc └─┘ ┴
178 [is_noetherian α β] : is_noetherian α γ :=
id └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
src └───────────┘ └───────────┘
typ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
179 is_noetherian_of_surjective _ f.to_linear_map f.range
id └─────────────────────────┘ ┴└────────────┘ ┴└────┘
src └─────────────────────────┘ └────────────┘ └────┘
typ └─────────────────────────┘ ┴└────────────┘ ┴└────┘
180
181 instance is_noetherian_prod [is_noetherian α β]
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
182 [is_noetherian α γ] : is_noetherian α (β × γ) :=
id └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴
src └───────────┘ └───────────┘ ┴
typ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴
183 ⟨λ s, submodule.fg_of_fg_map_of_fg_inf_ker (linear_map.snd α β γ) (noetherian _) $
id ┴ └──────────────────────────────────┘ └────────────┘ ┴ ┴ ┴ └────────┘
src └──────────────────────────────────┘ └────────────┘ └────────┘
typ ┴ └──────────────────────────────────┘ └────────────┘ ┴ ┴ ┴ └────────┘
doc └──────────────────────────────────┘ └────────────┘
184 have s ⊓ linear_map.ker (linear_map.snd α β γ) ≤ linear_map.range (linear_map.inl α β γ),
id ┴ ┴ └────────────┘ └────────────┘ ┴ ┴ ┴ ┴ └──────────────┘ └────────────┘ ┴ ┴ ┴
src ┴ └────────────┘ └────────────┘ ┴ └──────────────┘ └────────────┘
typ ┴ ┴ └────────────┘ └────────────┘ ┴ ┴ ┴ ┴ └──────────────┘ └────────────┘ ┴ ┴ ┴
doc └────────────┘ └────────────┘ └──────────────┘ └────────────┘
185 from λ x ⟨hx1, hx2⟩, ⟨x.1, trivial, prod.ext rfl $ eq.symm $ linear_map.mem_ker.1 hx2⟩,
id ┴ ┴ └─┘ ┴┴ └─────┘ └──────┘ └─┘ └─────┘ └────────────────┘┴
src ┴ └─────┘ └──────┘ └─┘ └─────┘ └────────────────┘┴
typ ┴ ┴ └─┘ ┴┴ └─────┘ └──────┘ └─┘ └─────┘ └────────────────┘┴
186 linear_map.map_comap_eq_self this ▸ submodule.fg_map (noetherian _)⟩
id └──────────────────────────┘ └──┘ ┴ └──────────────┘ └────────┘
src └──────────────────────────┘ ┴ └──────────────┘ └────────┘
typ └──────────────────────────┘ └──┘ ┴ └──────────────┘ └────────┘
187
188 instance is_noetherian_pi {α ι : Type*} {β : ι → Type*} [ring α]
id ┴ └──┘ ┴
src └──┘
typ ┴ └──┘ ┴
189 [Π i, add_comm_group (β i)] [Π i, module α (β i)] [fintype ι]
id ┴ └────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └─────┘ ┴
src └────────────┘ └────┘ └─────┘
typ ┴ └────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └─────┘ ┴
doc └────┘ └─────┘
190 [∀ i, is_noetherian α (β i)] : is_noetherian α (Π i, β i) :=
id ┴ └───────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴
src └───────────┘ └───────────┘
typ ┴ └───────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴
191 begin
st └─────
192 haveI := classical.dec_eq ι,
id └──────────────┘ ┴
src └───────┘└──────────────┘┴
typ └───────┘└──────────────┘┴┴
doc └───────┘ ┴
txt └───────┘ ┴
par └───────┘ ┴
pid ┴└─┘ ┴
st ────────────────────────────┘└─
193 suffices : ∀ s : finset ι, is_noetherian α (Π i : (↑s : set ι), β i),
id └────┘ └───────────┘ ┴ ┴┴ └─┘ ┴ ┴
src └─────────┘ └───┘└────┘┴ ┴└───────────┘┴ ┴ └───┘ ┴ └─┘└─┘┴ ┴ ┴ ┴ ┴
typ └─────────┘ └───┘└────┘┴ ┴└───────────┘┴┴┴ └───┘┴┴ └─┘└─┘┴┴┴ ┴┴┴ ┴
doc └─────────┘ └───┘└────┘┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ ┴ ┴
txt └─────────┘ └───┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ ┴ ┴
par └─────────┘ └───┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ ┴ ┴
pid └───────┘└┘ └───┘ ┴ ┴ ┴ ┴ └───┘ └─┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────┘└─
194 { letI := this finset.univ,
id └──┘ └─────────┘
src └──────┘ ┴└─────────┘
typ └──────┘└──┘┴└─────────┘
doc └──────┘ ┴└─────────┘
txt └──────┘ ┴
par └──────┘ ┴
pid ┴└─┘ ┴
st ───┘└──────────────────────┘└─
195 refine @is_noetherian_of_linear_equiv _ _ _ _ _ _ _ _
id └───────────────────────────┘
src └─────┘ └───────────────────────────┘└────────────────
typ └─────┘ └───────────────────────────┘└────────────────
doc └─────┘ └────────────────
txt └─────┘ └────────────────
par └─────┘ └────────────────
pid ┴ └────────────────
st ──────────────────────────────────────────────────────────
196 ⟨_, _, _, _, _, _⟩ (this finset.univ),
id └──┘ └─────────┘
src ─────┘ └────────────────┘ ┴└─────────┘┴
typ ─────┘ └────────────────┘ └──┘┴└─────────┘┴
doc ─────┘ └────────────────┘ ┴└─────────┘┴
txt ─────┘ └────────────────┘ ┴ ┴
par ─────┘ └────────────────┘ ┴ ┴
pid ─────┘ └────────────────┘ ┴ ┴
st ──────────────────────────────────────────┘
197 { exact λ f i, f ⟨i, finset.mem_univ _⟩ },
id └─────────────┘
src └────┘ └────┘ ┴ └┘└─────────────┘└──┘
typ └────┘ └────┘ ┴ └┘└─────────────┘└──┘
doc └────┘ └────┘ ┴ └┘ └──┘
txt └────┘ └────┘ ┴ └┘ └──┘
par └────┘ └────┘ ┴ └┘ └──┘
pid ┴ └────┘ ┴ └┘ └─┘┴
st └────────────────────────────────────┘┴
198 { intros, ext, refl },
src └────┘ └─┘
typ └────┘ └─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
st └────┘ └──┘ ┴
199 { intros, ext, refl },
st ┴
200 { exact λ f i, f i.1 },
st ┴
201 { intro, ext i, cases i, refl },
st ┴
202 { intro, ext i, refl } },
st └──┘┴
203 intro s,
204 induction s using finset.induction with a s has ih,
id ┴
typ ┴
205 { split, intro s, convert submodule.fg_bot, apply eq_bot_iff.2,
206 intros x hx, refine (submodule.mem_bot α).2 _, ext i, cases i.2 },
id ┴
typ ┴
st └┘
207 refine @is_noetherian_of_linear_equiv _ _ _ _ _ _ _ _
208 ⟨_, _, _, _, _, _⟩ (@is_noetherian_prod _ (β a) _ _ _ _ _ _ _ ih),
id ┴ ┴
typ ┴ ┴
209 { exact λ f i, or.by_cases (finset.mem_insert.1 i.2)
210 (λ h : i.1 = a, show β i.1, from (eq.rec_on h.symm f.1))
id ┴
typ ┴
211 (λ h : i.1 ∈ s, show β i.1, from f.2 ⟨i.1, h⟩) },
id ┴ ┴
typ ┴ ┴
st └┘
212 { intros f g, ext i, unfold or.by_cases, cases i with i hi,
213 rcases finset.mem_insert.1 hi with rfl | h,
214 { change _ = _ + _, simp only [dif_pos], refl },
st └┘
215 { change _ = _ + _, have : ¬i = a, { rintro rfl, exact has h },
id ┴ ┴
typ ┴ ┴
st └┘
216 simp only [dif_neg this, dif_pos h], refl } },
id └──┘
typ └──┘
st └──┘
217 { intros c f, ext i, unfold or.by_cases, cases i with i hi,
218 rcases finset.mem_insert.1 hi with rfl | h,
219 { change _ = c • _, simp only [dif_pos], refl },
id ┴
typ ┴
st └┘
220 { change _ = c • _, have : ¬i = a, { rintro rfl, exact has h },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
221 simp only [dif_neg this, dif_pos h], refl } },
id └──┘
typ └──┘
st └──┘
222 { exact λ f, (f ⟨a, finset.mem_insert_self _ _⟩, λ i, f ⟨i.1, finset.mem_insert_of_mem i.2⟩) },
id ┴
typ ┴
st └┘
223 { intro f, apply prod.ext,
224 { simp only [or.by_cases, dif_pos] },
st └┘
225 { ext i, cases i with i his,
226 have : ¬i = a, { rintro rfl, exact has his },
id ┴ ┴
typ ┴ ┴
st └┘
227 dsimp only [or.by_cases], change i ∈ s at his,
id ┴ ┴
typ ┴ ┴
228 rw [dif_neg this, dif_pos his] } },
id └──┘
typ └──┘
st ┴ └──┘
229 { intro f, ext i, cases i with i hi,
230 rcases finset.mem_insert.1 hi with rfl | h,
231 { simp only [or.by_cases, dif_pos], refl },
st └┘
232 { have : ¬i = a, { rintro rfl, exact has h },
id ┴ ┴
typ ┴ ┴
st └┘
233 simp only [or.by_cases, dif_neg this, dif_pos h], refl } }
id └──┘
typ └──┘
st └───
234 end
st ──┘
235
236 end
237
238 open is_noetherian submodule function
239
240 theorem is_noetherian_iff_well_founded
241 {α β} [ring α] [add_comm_group β] [module α β] :
id └┘ └──┘ └──┘ └┘ ┴ ┴
src └┘ └──┘ └──┘ └┘
typ └┘ └──┘ └──┘ └┘ ┴ ┴
242 is_noetherian α β ↔ well_founded ((>) : submodule α β → submodule α β → Prop) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
243 ⟨λ h, begin
244 apply order_embedding.well_founded_iff_no_descending_seq.2,
245 swap, { apply is_strict_order.swap },
st └┘
246 rintro ⟨⟨N, hN⟩⟩,
247 let M := ⨆ n, N n,
id ┴
typ ┴
248 resetI,
249 rcases submodule.fg_def.1 (noetherian M) with ⟨t, h₁, h₂⟩,
250 have hN' : ∀ {a b}, a ≤ b → N a ≤ N b :=
id ┴ ┴
src ┴
typ ┴ ┴
251 λ a b, (strict_mono.le_iff_le (λ _ _, hN.1)).2,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
252 have : t ⊆ ⋃ i, (N i : set β),
id ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ └─┘ ┴
253 { rw [← submodule.Union_coe_of_directed _ N _],
254 { show t ⊆ M, rw ← h₂,
id ┴
typ ┴
255 apply submodule.subset_span },
st └┘
256 { apply_instance },
st └┘
257 { exact λ i j, ⟨max i j,
id ┴ ┴
typ ┴ ┴
258 hN' (le_max_left _ _),
259 hN' (le_max_right _ _)⟩ } },
st └──┘
260 simp [subset_def] at this,
261 choose f hf using show ∀ x : t, ∃ (i : ℕ), x.1 ∈ N i, { simpa },
st └┘
262 cases h₁ with h₁,
id └┘
typ └┘
263 let A := finset.sup (@finset.univ t h₁) f,
id ┴
typ ┴
264 have : M ≤ N A,
id ┴
typ ┴
265 { rw ← h₂, apply submodule.span_le.2,
266 exact λ x h, hN' (finset.le_sup (@finset.mem_univ t h₁ _))
id ┴ ┴
typ ┴ ┴
267 (hf ⟨x, h⟩) },
st └┘
268 exact not_le_of_lt (hN.1 (nat.lt_succ_self A))
id ┴
typ ┴
269 (le_trans (le_supr _ _) this)
270 end,
st └─┘
271 begin
272 assume h, split, assume N,
273 suffices : ∀ M ≤ N, ∃ s, finite s ∧ M ⊔ submodule.span α s = N,
id ┴ ┴
typ ┴ ┴
274 { rcases this ⊥ bot_le with ⟨s, hs, e⟩,
275 exact submodule.fg_def.2 ⟨s, hs, by simpa using e⟩ },
id ┴ └┘
typ ┴ └┘
st └┘
276 refine λ M, h.induction M _, intros M IH MN,
277 letI := classical.dec,
id └───────────┘
src └───────────┘
typ └───────────┘
278 by_cases h : ∀ x, x ∈ N → x ∈ M,
id ┴
typ ┴
279 { cases le_antisymm MN h, exact ⟨∅, by simp⟩ },
st └┘
280 { simp [not_forall] at h,
281 rcases h with ⟨x, h, h₂⟩,
282 have : ¬M ⊔ submodule.span α {x} ≤ M,
id ┴ ┴
typ ┴ ┴
283 { intro hn, apply h₂,
284 have := le_trans le_sup_right hn,
285 exact submodule.span_le.1 this (mem_singleton x) },
id ┴
typ ┴
st └┘
286 rcases IH (M ⊔ submodule.span α {x})
id ┴ ┴
typ ┴ ┴
287 ⟨@le_sup_left _ _ M _, this⟩
288 (sup_le MN (submodule.span_le.2 (by simpa))) with ⟨s, hs, hs₂⟩,
289 refine ⟨insert x s, finite_insert _ hs, _⟩,
id ┴ ┴ └┘
typ ┴ ┴ └┘
290 rw [← hs₂, sup_assoc, ← submodule.span_union], simp }
st └┘
291 end⟩
st └─┘
292
293 lemma well_founded_submodule_gt (α β) [ring α] [add_comm_group β] [module α β] :
id └──┘ └──┘ └──┘ └┘ ┴ ┴ ┴
src └──┘ └──┘ └──┘ └┘
typ └──┘ └──┘ └──┘ └┘ ┴ ┴ ┴
294 ∀ [is_noetherian α β], well_founded ((>) : submodule α β → submodule α β → Prop) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
295 is_noetherian_iff_well_founded.mp
296
297 lemma finite_of_linear_independent {α β} [nonzero_comm_ring α] [add_comm_group β] [module α β]
id ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └──┘ └──┘ ┴ ┴ ┴
src ┴ └┘ └┘ └┘ └┘ └┘ └┘ └──┘ └──┘
typ ┴ └┘ └┘ └┘ └┘ └┘ ┴ └┘ └──┘ └──┘ ┴ ┴ ┴
doc ┴ └┘ └┘ └┘ └┘ └┘
298 [is_noetherian α β] {s : set β} (hs : linear_independent α (subtype.val : s → β)) : s.finite :=
id ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └┘
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴
299 begin
300 refine classical.by_contradiction (λ hf, order_embedding.well_founded_iff_no_descending_seq.1
301 (well_founded_submodule_gt α β) ⟨_⟩),
302 have f : ℕ ↪ s, from @infinite.nat_embedding s ⟨λ f, hf ⟨f⟩⟩,
id ┴ ┴ ┴ └┘
src ┴
typ ┴ ┴ ┴ └┘
303 have : ∀ n, (subtype.val ∘ f) '' {m | m ≤ n} ⊆ s,
id ┴ ┴ ┴
typ ┴ ┴ ┴
304 { rintros n x ⟨y, hy₁, hy₂⟩, subst hy₂, exact (f y).2 },
id ┴
typ ┴
st └┘
305 have : ∀ a b : ℕ, a ≤ b ↔
306 span α ((subtype.val ∘ f) '' {m | m ≤ a}) ≤ span α ((subtype.val ∘ f) '' {m | m ≤ b}),
id ┴ ┴ ┴
typ ┴ ┴ ┴
307 { assume a b,
308 rw [span_le_span_iff (@zero_ne_one α _) hs (this a) (this b),
id ┴ ┴ ┴
typ ┴ ┴ ┴
309 set.image_subset_image_iff (injective_comp subtype.val_injective f.inj'),
310 set.subset_def],
311 exact ⟨λ hab x (hxa : x ≤ a), le_trans hxa hab, λ hx, hx a (le_refl a)⟩ },
id └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴
st └┘
312 exact ⟨⟨λ n, span α ((subtype.val ∘ f) '' {m | m ≤ n}),
id ┴ ┴ ┴
typ ┴ ┴ ┴
313 λ x y, by simp [le_antisymm_iff, (this _ _).symm] {contextual := tt}⟩,
id ┴ ┴ └┘
src └┘
typ ┴ ┴ └┘
314 by dsimp [gt]; simp only [lt_iff_le_not_le, (this _ _).symm]; tauto⟩
315 end
st └─┘
316
317 @[class] def is_noetherian_ring (α) [ring α] : Prop := is_noetherian α α
id └──┘ ┴ ┴
src └──┘
typ └──┘ ┴ ┴
318
319 instance is_noetherian_ring.to_is_noetherian {α : Type*} [ring α] :
id └┘ ┴
src └┘
typ └┘ ┴
320 ∀ [is_noetherian_ring α], is_noetherian α α := id
id ┴ ┴ ┴
typ ┴ ┴ ┴
321
322 @[priority 80] -- see Note [lower instance priority]
323 instance ring.is_noetherian_of_fintype (R M) [fintype M] [ring R] [add_comm_group M] [module R M] : is_noetherian R M :=
id └─────┘ ┴ └──┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──┘ └────────────┘
typ └─────┘ ┴ └──┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘
324 by letI := classical.dec; exact
id └───────────┘
src └───────────┘
typ └───────────┘
325 ⟨assume s, ⟨to_finset s, by rw [finset.coe_to_finset', submodule.span_eq]⟩⟩
st ┴
326
327 theorem ring.is_noetherian_of_zero_eq_one {R} [ring R] (h01 : (0 : R) = 1) : is_noetherian_ring R :=
id └──┘ ┴ ┴
src └──┘
typ └──┘ ┴ ┴
328 by haveI := subsingleton_of_zero_eq_one R h01;
id ┴
typ ┴
329 haveI := fintype.of_subsingleton (0:R);
id ┴
typ ┴
330 exact ring.is_noetherian_of_fintype _ _
331
332 theorem is_noetherian_of_submodule_of_noetherian (R M) [ring R] [add_comm_group M] [module R M] (N : submodule R M)
id └┘ ┴ └──┘ └──┘ └┘ ┴ ┴ ┴ ┴ ┴
src └┘ └──┘ └──┘ └┘
typ └┘ ┴ └──┘ └──┘ └┘ ┴ ┴ ┴ ┴ ┴
333 (h : is_noetherian R M) : is_noetherian R N :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
334 begin
335 rw is_noetherian_iff_well_founded at h ⊢,
336 convert order_embedding.well_founded (order_embedding.rsymm (submodule.map_subtype.lt_order_embedding N)) h
337 end
st └─┘
338
339 theorem is_noetherian_of_quotient_of_noetherian (R) [ring R] (M) [add_comm_group M] [module R M] (N : submodule R M)
id └┘ ┴ └──┘ └──┘ └┘ ┴ ┴ ┴ ┴ ┴
src └┘ └──┘ └──┘ └┘
typ └┘ ┴ └──┘ └──┘ └┘ ┴ ┴ ┴ ┴ ┴
340 (h : is_noetherian R M) : is_noetherian R N.quotient :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
341 begin
342 rw is_noetherian_iff_well_founded at h ⊢,
343 convert order_embedding.well_founded (order_embedding.rsymm (submodule.comap_mkq.lt_order_embedding N)) h
344 end
st └─┘
345
346 theorem is_noetherian_of_fg_of_noetherian {R M} [ring R] [add_comm_group M] [module R M] (N : submodule R M)
id └┘ └──┘ └──┘ └┘ ┴ ┴ ┴ ┴ ┴
src └┘ └──┘ └──┘ └┘
typ └┘ └──┘ └──┘ └┘ ┴ ┴ ┴ ┴ ┴
347 [is_noetherian_ring R] (hN : N.fg) : is_noetherian R N :=
id ┴ ┴
typ ┴ ┴
348 let ⟨s, hs⟩ := hN in
349 begin
350 haveI := classical.dec_eq M,
id ┴
typ ┴
351 haveI := classical.dec_eq R,
id ┴
typ ┴
352 letI : is_noetherian R R := by apply_instance,
id ┴
typ ┴
353 have : ∀ x ∈ s, x ∈ N, from λ x hx, hs ▸ submodule.subset_span hx,
id ┴ ┴
typ ┴ ┴
354 refine @@is_noetherian_of_surjective ((↑s : set M) → R) _ _ _ (pi.module _)
id ┴ └─┘ ┴ ┴
src └─┘
typ ┴ └─┘ ┴ ┴
355 _ _ _ is_noetherian_pi,
356 { fapply linear_map.mk,
357 { exact λ f, ⟨s.attach.sum (λ i, f i • i.1), N.sum_mem (λ c _, N.smul_mem _ $ this _ c.2)⟩ },
st └┘
358 { intros f g, apply subtype.eq,
359 change s.attach.sum (λ i, (f i + g i) • _) = _,
360 simp only [add_smul, finset.sum_add_distrib], refl },
st └┘
361 { intros c f, apply subtype.eq,
362 change s.attach.sum (λ i, (c • f i) • _) = _,
id ┴
typ ┴
363 simp only [smul_eq_mul, mul_smul],
364 exact s.attach.sum_hom _ } },
st └──┘
365 rw linear_map.range_eq_top,
366 rintro ⟨n, hn⟩, change n ∈ N at hn,
id ┴
typ ┴
367 rw [← hs, ← set.image_id ↑s, finsupp.mem_span_iff_total] at hn,
id ┴
typ ┴
368 rcases hn with ⟨l, hl1, hl2⟩,
369 refine ⟨λ x, l x.1, subtype.eq _⟩,
370 change s.attach.sum (λ i, l i.1 • i.1) = n,
id ┴
typ ┴
371 rw [@finset.sum_attach M M s _ (λ i, l i • i), ← hl2,
id ┴ ┴ ┴
typ ┴ ┴ ┴
372 finsupp.total_apply, finsupp.sum, eq_comm],
373 refine finset.sum_subset hl1 (λ x _ hx, _),
id ┴
typ ┴
374 rw [finsupp.not_mem_support_iff.1 hx, zero_smul]
st ┴
375 end
st └─┘
376
377 /-- In a module over a noetherian ring, the submodule generated by finitely many vectors is
378 noetherian. -/
379 theorem is_noetherian_span_of_finite (R) {M} [ring R] [add_comm_group M] [module R M] [is_noetherian_ring R]
id └┘ ┴ └──┘ └──┘ └┘ ┴ ┴ ┴ ┴
src └┘ └──┘ └──┘ └┘
typ └┘ ┴ └──┘ └──┘ └┘ ┴ ┴ ┴ ┴
380 {A : set M} (hA : finite A) : is_noetherian R (submodule.span R A) :=
id └┘ ┴ ┴ ┴ ┴ ┴
src └┘
typ └┘ ┴ ┴ ┴ ┴ ┴
381 is_noetherian_of_fg_of_noetherian _ (submodule.fg_def.mpr ⟨A, hA, rfl⟩)
id ┴ └┘
typ ┴ └┘
382
383 theorem is_noetherian_ring_of_surjective (R) [comm_ring R] (S) [comm_ring S]
id ┴ └┘ └┘ ┴ ┴ └──┘ └┘ ┴
src ┴ └┘ └┘ ┴ └──┘ └┘
typ ┴ └┘ └┘ ┴ ┴ └──┘ └┘ ┴
384 (f : R → S) [is_ring_hom f] (hf : function.surjective f)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
385 [H : is_noetherian_ring R] : is_noetherian_ring S :=
id ┴ ┴
typ ┴ ┴
386 begin
387 unfold is_noetherian_ring at H ⊢,
388 rw is_noetherian_iff_well_founded at H ⊢,
389 convert order_embedding.well_founded (order_embedding.rsymm (ideal.lt_order_embedding_of_surjective f hf)) H
id ┴ └┘
typ ┴ └┘
390 end
st └─┘
391
392 instance is_noetherian_ring_range {R} [comm_ring R] {S} [comm_ring S] (f : R → S) [is_ring_hom f]
id └──┘ └─┘ ┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴
src └──┘ └─┘ └┘ └┘ └┘
typ └──┘ └─┘ ┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴
393 [is_noetherian_ring R] : is_noetherian_ring (set.range f) :=
id ┴ ┴
typ ┴ ┴
394 @is_noetherian_ring_of_surjective R _ (set.range f) _ (λ x, ⟨f x, x, rfl⟩)
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
395 (⟨subtype.eq (is_ring_hom.map_one f),
id ┴
typ ┴
396 λ _ _, subtype.eq (is_ring_hom.map_mul f),
id ┴ ┴ ┴
typ ┴ ┴ ┴
397 λ _ _, subtype.eq (is_ring_hom.map_add f)⟩)
id ┴ ┴ ┴
typ ┴ ┴ ┴
398 (λ ⟨x, y, hy⟩, ⟨y, subtype.eq hy⟩) _
id ┴ ┴
typ ┴ ┴
399
400 theorem is_noetherian_ring_of_ring_equiv (R) [comm_ring R] {S} [comm_ring S]
id └──┘ └─┘ ┴ └┘ └┘ └┘ ┴
src └──┘ └─┘ └┘ └┘ └┘
typ └──┘ └─┘ ┴ └┘ └┘ └┘ ┴
401 (f : R ≃+* S) [is_noetherian_ring R] : is_noetherian_ring S :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
402 is_noetherian_ring_of_surjective R S f.1 f.to_equiv.surjective
id ┴ ┴
typ ┴ ┴
403
404 namespace is_noetherian_ring
405
406 variables {α : Type*} [integral_domain α] [is_noetherian_ring α]
id └┘ └┘ └┘ └┘ └┘
src └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ └┘
407 open associates nat
408
409 local attribute [elab_as_eliminator] well_founded.fix
doc └────────────────┘
410
411 lemma well_founded_dvd_not_unit : well_founded (λ a b : α, a ≠ 0 ∧ ∃ x, ¬is_unit x ∧ b = a * x ) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
412 by simp only [ideal.span_singleton_lt_span_singleton.symm];
413 exact inv_image.wf (λ a, ideal.span ({a} : set α)) (well_founded_submodule_gt _ _)
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
414
415 lemma exists_irreducible_factor {a : α} (ha : ¬ is_unit a) (ha0 : a ≠ 0) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
416 ∃ i, irreducible i ∧ i ∣ a :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
417 (irreducible_or_factor a ha).elim (λ hai, ⟨a, hai, dvd_refl _⟩)
id ┴ ┴
typ ┴ ┴
418 (well_founded.fix
419 well_founded_dvd_not_unit
420 (λ a ih ha ha0 ⟨x, y, hx, hy, hxy⟩,
id ┴ ┴ ┴
typ ┴ ┴ ┴
421 have hx0 : x ≠ 0, from λ hx0, ha0 (by rw [← hxy, hx0, zero_mul]),
st ┴
422 (irreducible_or_factor x hx).elim
423 (λ hxi, ⟨x, hxi, hxy ▸ by simp⟩)
424 (λ hxf, let ⟨i, hi⟩ := ih x ⟨hx0, y, hy, hxy.symm⟩ hx hx0 hxf in
id ┴
typ ┴
425 ⟨i, hi.1, dvd.trans hi.2 (hxy ▸ by simp)⟩)) a ha ha0)
id ┴
typ ┴
426
427 @[elab_as_eliminator] lemma irreducible_induction_on {P : α → Prop} (a : α)
id ┴
typ ┴
doc └────────────────┘
428 (h0 : P 0) (hu : ∀ u : α, is_unit u → P u)
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
429 (hi : ∀ a i : α, a ≠ 0 → irreducible i → P a → P (i * a)) :
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
430 P a :=
id ┴
typ ┴
431 by haveI := classical.dec; exact
id └───────────┘
src └───────────┘
typ └───────────┘
432 well_founded.fix well_founded_dvd_not_unit
433 (λ a ih, if ha0 : a = 0 then ha0.symm ▸ h0
id ┴
typ ┴
434 else if hau : is_unit a then hu a hau
435 else let ⟨i, hii, ⟨b, hb⟩⟩ := exists_irreducible_factor hau ha0 in
id ┴ ┴
typ ┴ ┴
436 have hb0 : b ≠ 0, from λ hb0, by simp * at *,
437 hb.symm ▸ hi _ _ hb0 hii (ih _ ⟨hb0, i,
438 hii.1, by rw [hb, mul_comm]⟩))
st ┴
439 a
id ┴
typ ┴
440
441 lemma exists_factors (a : α) : a ≠ 0 →
id ┴ ┴
typ ┴ ┴
442 ∃f:multiset α, (∀b∈f, irreducible b) ∧ associated a f.prod :=
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
443 is_noetherian_ring.irreducible_induction_on a
id ┴
typ ┴
444 (λ h, (h rfl).elim)
445 (λ u hu _, ⟨0, by simp [associated_one_iff_is_unit, hu]⟩)
id ┴
typ ┴
446 (λ a i ha0 hii ih hia0,
id ┴ ┴
typ ┴ ┴
447 let ⟨s, hs⟩ := ih ha0 in
id ┴
typ ┴
448 ⟨i::s, ⟨by clear _let_match; finish,
id ┴
typ ┴
449 by rw multiset.prod_cons;
450 exact associated_mul_mul (by refl) hs.2⟩⟩)
451
452 end is_noetherian_ring
453
454 namespace submodule
455 variables {R : Type*} {A : Type*} [comm_ring R] [ring A] [algebra R A]
id ┴ └─┘ └─┘ └┘
src ┴ └─┘ └─┘ └┘
typ ┴ └─┘ └─┘ └┘
456 variables (M N : submodule R A)
457
458 local attribute [instance] set.pointwise_mul_semiring
459
460 theorem fg_mul (hm : M.fg) (hn : N.fg) : (M * N).fg :=
461 let ⟨m, hfm, hm⟩ := fg_def.1 hm, ⟨n, hfn, hn⟩ := fg_def.1 hn in
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
462 fg_def.2 ⟨m * n, set.pointwise_mul_finite hfm hfn, span_mul_span R m n ▸ hm ▸ hn ▸ rfl⟩
id ┴
typ ┴
463
464 lemma fg_pow (h : M.fg) (n : ℕ) : (M^n).fg :=
id ┴ ┴
src ┴
typ ┴ ┴
465 nat.rec_on n
id ┴
typ ┴
466 (⟨finset.singleton 1, by simp [one_eq_span]⟩)
467 (λ n ih, by simpa [pow_succ] using fg_mul _ _ h ih)
id ┴
typ ┴
468
469 end submodule